|
Japaridze's polymodal logic (GLP), is a system of provability logic with infinitely many modal (provability) operators. This system has played an important role in some applications of provability algebras in proof theory, and has been extensively studied since the late 1980s. It is named after Giorgi Japaridze. == Language and axiomatization == The language of GLP extends that of the language of classical propositional logic by including the infinite series (),(),(),... of “necessity” operators. Their dual “possibility” operators <0>,<1>,<2>,... are defined by <''n''>''p'' = ¬()¬''p''. The axioms of GLP are all classical tautologies and all formulas of one of the following forms: *()(''p'' → ''q'') → (()''p'' → ()''q'') *()(()''p'' → ''p'') → ()''p'' *()''p'' → ()''p'' *<''n''>''p'' → ()<''n''>''p'' And the rules of inference are: * From ''p'' and ''p'' → ''q'' conclude ''q'' * From ''p'' conclude ()''p'' 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Japaridze's polymodal logic」の詳細全文を読む スポンサード リンク
|